b:, a:. y:. GCD(a;b;y) 

latex

Definitions	Prop, AB, A, False, x:A. B(x), GCD(a;b;y), ij, P  Q, , x:A. B(x), t  T, Dec(P), P  Q, P  Q, P & Q, T, P  Q, True, , {i..j}, i  j < k
Lemmas	gcd p shift, add com, gcd p sym, quot rem exists, gcd p zero, gcd p wf, true wf, squash wf, decidable int equal, nat wf, nat properties, ge wf, le wf